T:Type, L:(T List), P:({x:T| (x  L)} ), T':Type, f:({x:T| (x  L) c ((P(x)))} T'), x:T'.
(x  mapfilter(f;P;L))  (y:T. ((y  L) & (((P(y))) c (x = f(y))))) 

latex

Definitions	(x  l), , suptype(S; T), S  T, A c B, b, x:A. B(x), t  T, P  Q, P  Q, P  Q, x:A. B(x), P & Q, , l[i], , A  B, A, False, ||as||, SQType(T), {T}, mapfilter(f;P;L), map(f;as), filter(P;l), type List, Type, f(a), x:AB(x), x:A  B(x), {x:A| B(x)}
Lemmas	l member-set, subtype rel list, filter type, filter wf, map wf, nat wf, select wf, length wf1, list-subtype, l member wf, assert wf, member map filter, bool wf